Nuprl Lemma : Tactics as terms 13,42

ABS: skip{a}

ABS: let $x = a in b

ABS: THENL(al)

ABS: (a THENM b)

ABS: (a THENA b)

ABS: (a THEN b)

ABS: (a ORELSE b)

ABS: (Assert a BY b)

ABS: Decide a

ABS: Try (a)

ABS: Complete (a)

ABS: RepeatFor $n (a)

ABS: SplitOnHypITE $n 

ABS: HypSubst' $dir $a $b

ABS: Subst' x $b

ABS: BHyp $a 

ABS: D $a

ABS: ExRepD

ABS: Auto

ABS: MaAuto

ABS: Unfold `$ab` $hyp

ABS: Unfolds ``$abs`` $hyp

ABS: RepUR ``$abs`` $hyp

ABS: ParallelOp $hyp

ABS: Branch3

ABS: Branch2

ABS: OnMaybeHyp $h (\h. tactic)

ABS: EsReal `$opid` tokens


UpEventSystems

origin